|
|
Verifikace ASIP založena na formálních tvrzeních
Šulek, Jakub ; Dolíhal, Luděk (oponent) ; Zachariášová, Marcela (vedoucí práce)
Tato práce představuje koncept pro ověřování správnosti procesorů s aplikačně-specifickou instrukční sadou (ASIP) pomocí verifi kace založené na formálních tvrzeních. Koncept je implementován v jazyku SystemVerilog Assertions jako součást verifi kačního prostředí vytvořeného v nástroji Codasip Framework. Implementovaný koncept je simulován nástrojem QuestaSim na procesoru Codix RISC. Hlavním výsledkem práce je koncept ověřování, který může být součástí systému automatizujícího návrh procesorů, a který je použitelný pro různé typy procesorů.
|
|
|
Formal verification of RISC-V processor with Questa PropCheck
Javor, Adrián ; Fujcik, Lukáš (oponent) ; Dvořák, Vojtěch (vedoucí práce)
The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.
|
|
|
Formal verification of RISC-V processor with Questa PropCheck
Javor, Adrián ; Fujcik, Lukáš (oponent) ; Dvořák, Vojtěch (vedoucí práce)
The topic of this master thesis is Formal verification of RISC-V processor with Questa PropCheck using SystemVerilog assertions. The theoretical part writes about the RISC-V architecture, furthermore, selected components of Codix Berkelium 5 processor used for formal verification are described, communication protocol AHB-lite, formal verification and its methods and tools are also studied. Experimental part consists of verification planning of selected components, subsequent formal verification, analysing of results and evaluating a benefits of formal technics.
|
|
|
Verifikace ASIP založena na formálních tvrzeních
Šulek, Jakub ; Dolíhal, Luděk (oponent) ; Zachariášová, Marcela (vedoucí práce)
Tato práce představuje koncept pro ověřování správnosti procesorů s aplikačně-specifickou instrukční sadou (ASIP) pomocí verifi kace založené na formálních tvrzeních. Koncept je implementován v jazyku SystemVerilog Assertions jako součást verifi kačního prostředí vytvořeného v nástroji Codasip Framework. Implementovaný koncept je simulován nástrojem QuestaSim na procesoru Codix RISC. Hlavním výsledkem práce je koncept ověřování, který může být součástí systému automatizujícího návrh procesorů, a který je použitelný pro různé typy procesorů.
|
host ::
RSS.